L:( List), a:. (0 < ||L||)  ((a  imax-list(L))  (bL.a  b)) 

latex

Definitions	x:A. B(x), P  Q, P  Q, A  B, imax-list(L), {T}, t  T, Top, S  T, , Y, P & Q, P  Q, A, False, x. t(x), list_accum(x,a.f(x;a);y;l), hd(l), tl(l), P  Q, i  j , , ||as||, x(s)
Lemmas	nat wf, length wf nat, top wf, length wf1, le wf, imax-list wf, length wf2, l exists wf, iff functionality wrt iff, l exists cons, false wf, or functionality wrt iff, l exists nil, imax wf, length cons, non neg length, imax ub, nat properties, ge wf